Skip to content

TB: Track permissions on the byte-level #4314

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 15 commits into
base: master
Choose a base branch
from

Conversation

yoctocell
Copy link

This makes the tracking of permissions on the byte-level, like in Stacked Borrows, which makes the tracking of interior mutable data more fine-grained.

cc @RalfJung @JoJoDeveloping

@JoJoDeveloping
Copy link
Contributor

So, how does adding a new node work (and why do we need to call visit_freeze_sensitive three times:

  • First, you do a read access at the parent node
  • Then, you add the new node. Note that adding a new node is a per-block operation, not per-access
  • Then you set the correct permissions for the new node
  • Then you reset the SIFA thingy (also per-block)
  • Then you call into the data race model

For Stacked Borrows, there are no per-block operations: each stack at each offset its own stack and completely independent from the other ones at different offsets in the same allocation. So there, more (basically everything) can be moved into the per-offset function.

So what do we do for Tree Borrows? One answer is to combine parent reading, permission setting and data race notifying together. This would be somewhat ugly, because you're constructing a node, while also accessing the tree, and this would only be fine because you're careful to not actually add the node into the children array of its parent so that it's not visited when walking the tree.

Should we do this?

@RalfJung
Copy link
Member

Ignoring the SIFA thingy since I already forgot how it works, what I think would make sense is to do a single visit_freeze_sensitive where you

  • do the parent access
  • do the data race access
  • prepare a RangeMap<LocationState> of per-location initial states that will later be passed to Tree::new_child

Does that makes sense or is it too ugly as well?

@JoJoDeveloping
Copy link
Contributor

JoJoDeveloping commented May 12, 2025

That would work. It has to construct an extra RangeMap but presumably this is cheaper than calling visit_freeze_sensitive thrice.
And it requires moving some logic for retags around quite a bit.

@RalfJung
Copy link
Member

presumably this is cheaper than calling visit_freeze_sensitive thrice.

I'm not sure, but that's at least plausible. I also prefer it conceptually.

Xinglu Chen added 3 commits May 13, 2025 17:17
Previously, the assert would cause an error if the `RangeMap` was
empty.
Copy link
Member

@RalfJung RalfJung left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! This is a lot better.

I don't fully understand the logic around the new perms_map though. It seems like the map is created to cover all the bytes from the beginning of the allocation to the end of the retagged place, which is odd -- it should be either the entire allocation, or just the place. And given that we do not want to actually put anything into the perms map outside the place, I think it should be just the place.

Comment on lines 636 to 637
// SIFA of the frozen part must be weaker than SIFA of the non-frozen part, otherwise
// `self.update_last_accessed_after_retag` will break the SIFA invariant (see `foreign_access_skipping.rs`).
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't understand why this assertion must hold. foreign_access_skipping doesn't explain it either, it does not mention frozen vs non-frozen parts at all.

@RalfJung
Copy link
Member

I have pushed a commit with various minor cleanups -- please take a look, I hope they make sense. :)

However, in doing so I stumbled upon a question I could not answer.

@RalfJung RalfJung force-pushed the fine-grained-tracking branch from e705a08 to d518dcf Compare May 23, 2025 09:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants